DIR: chain sys object directory

STM: chain sys-cases

DIR: chain config object directory

STM: decidable exists-fail

ABS: fail-dcdr{i:l}(es;Fail)

STM: fail-dcdr wf

ABS: alive(X)

STM: alive wf

STM: es-is-alive

STM: es-alive-val

ABS: sys-cmds(x)

STM: sys-cmds wf

ABS: valid-sys(es;Config;Sys;e)

STM: valid-sys wf

STM: decidable valid-sys

ABS: valid-sys-dcdr{i:l}(es;Config;Cmd;Sys)

STM: valid-sys-dcdr wf

ABS: Sys(valid)

STM: sys-valid wf

STM: is-sys-valid

STM: sys-valid-subtype

STM: decidable input

ABS: input-dcdr{i:l}(es;Cmd;Sys)

STM: input-dcdr wf

ABS: Input

STM: cr-input wf

STM: cr-input-subtype

STM: is-cr-input

STM: decidable is-tail

ABS: tail-dcdr{i:l}(es;Config)

STM: tail-dcdr wf

ABS: Output

STM: cr-output wf

STM: cr-output-subtype

ABS: cmd-history(e)

STM: cmd-history wf

STM: nonempty-cmd-history

ABS: master-constraints(es;Master)

STM: master-constraints wf

ABS: config-antecedent(es;Master;Config;c)

STM: config-antecedent wf

ABS: master-antecedent{i:l}(es;Cmd;Master;Config;Sys;m)

STM: master-antecedent wf

ABS: update-antecedent{i:l}(es;Cmd;Sys;Config;u)

STM: update-antecedent wf

ABS: chain-replication{i:l}(es;Cmd;Sys;Config;Master;u)

STM: chain-replication wf

STM: update-antecedent-lemma1

ABS: cr-antecedent{i:l}(es;Config;Cmd;Sys;u)

STM: cr-antecedent wf